﻿using System;
using System.Collections.Generic;
using System.Text;

using System.Diagnostics.Contracts;

using SimpleIR;


namespace RgnAnalyzer.Domain
{
	public partial class AProgramMemory
	{
		/////////////////////////////////////////////////////////
		//traversal support

		internal enum VisitColor : byte { White = 0x0, Grey = 0x1, Black = 0x2 };

		/// <summary>
		/// A helper class for tracking info during DFS graph traversals.
		/// </summary>
		internal struct VisitInfo
		{
			internal VisitColor Color;
			internal short DiscoverTime;
			internal short FinishTime;

			internal VisitInfo(VisitColor vc, short tdiscover, short tfinish)
			{
				this.Color = vc;
				this.DiscoverTime = tdiscover;
				this.FinishTime = tfinish;
			}

			public override String ToString()
			{ return "(C=" + this.Color.ToString() + ", D=" + this.DiscoverTime.ToString() + ", F=" + this.FinishTime.ToString() + ")"; }
		}

		/// <summary>
		/// Fill the list with the set of all root --As in referenced from a name, NOT as in not incomming edges-- nodes for this graph (may contain duplicates).
		/// </summary>
		internal void FillRootSet(List<ALocation> rns, HashSet<AHomeLocation> statichomelocs)
		{
			HashSet<ALocation> roots = new HashSet<ALocation>();

			foreach(KeyValuePair<IRRootIdentifier, int> trv in this.m_nametonodemap)
			{
				roots.Add(this.m_memory[trv.Value]);

				if((statichomelocs != null) & (trv.Key is IRStaticField))
					statichomelocs.Add((AHomeLocation)this.m_memory[trv.Value]);
			}

			foreach(int[] tnid in this.m_externalrefs.Values)
			{
				for(int i = 0; i < tnid.Length; ++i)
					roots.Add(this.m_memory[tnid[i]]);
			}

			for(int i = 0; i < this.m_evalstack.Count; ++i)
			{
				AEvalStackEntry sn = this.m_evalstack[i];
				if(!(sn.SLocType is IRFunctionPointerType))
				{
					IEnumerator<ATrgtEnum> evse = sn.GetATrgtEnumerator();
					while(evse.MoveNext())
					{
						ALocation aloc = this.ResolveRawAddress(evse.Current.TrgtAddress);
						roots.Add(aloc);
					}
				}
			}

			rns.AddRange(roots);
		}

		/// <summary>
		/// Do a DFS computing the visited info into vinfo, sorted nodes into revsorted list and using a given root set to start the traversal.
		/// </summary>
		internal void DoDFS(VisitInfo[] vinfo)
		{
			Contract.Requires(!this.IsInfeasable);
			Contract.Requires(vinfo != null);
			Contract.Assert(this.m_memory.Count == vinfo.Length);

			List<ALocation> roots = new List<ALocation>();
			this.FillRootSet(roots, null);

			short ctime = 1;
			for(int i = 0; i < roots.Count; ++i)
			{
				ALocation nn = roots[i];
				this.DoDFSVisit(nn, vinfo, null, ref ctime);
			}
		}

		/// <summary>
		/// Do a DFS computing the visited info into vinfo, sorted nodes into revsorted list and using a given root set to start the traversal.
		/// </summary>
		internal void DoDFS(List<ALocation> roots, List<ALocation> revsortedlist, VisitInfo[] vinfo)
		{
			Contract.Requires(!this.IsInfeasable);
			Contract.Requires(roots != null);
			Contract.Requires(vinfo != null);
			Contract.Assert(this.m_memory.Count == vinfo.Length);

			short ctime = 1;
			foreach(ALocation nn in roots)
				this.DoDFSVisit(nn, vinfo, revsortedlist, ref ctime);
		}

		internal void DoDFSVisit(ALocation aloc, VisitInfo[] vinfo, List<ALocation> revsortedlist, ref short ctime)
		{
			Contract.Requires(!this.IsInfeasable);
			Contract.Requires(aloc != null);

			if(vinfo[aloc.Address].Color != VisitColor.White)
				return;

			VisitInfo dinfo = new VisitInfo(VisitColor.Grey, ctime++, 0);
			vinfo[aloc.Address] = dinfo;

			IEnumerator<ATrgtEnum> trgtenum = aloc.GetTargetEnum();
			while(trgtenum.MoveNext())
			{
				ATrgtEnum te = trgtenum.Current;
				ALocation trgtloc = this.ResolveRawAddress(te.TrgtAddress);
				this.DoDFSVisit(trgtloc, vinfo, revsortedlist, ref ctime);
			}

			VisitInfo finfo = new VisitInfo(VisitColor.Black, dinfo.DiscoverTime, ctime++);
			vinfo[aloc.Address] = finfo;

			if(revsortedlist != null)
				revsortedlist.Add(aloc);
		}

		/////////////////////////////////////////////////////////
		//support for compaction/transfer/compare operations

		/// <summary>
		/// Clear all the nodes that are no longer live (e.g. not reachable from any root or external reference).
		/// </summary>
		internal void ClearUnreachableNodes()
		{
			VisitInfo[] vinfo = new VisitInfo[this.m_memory.Count];
			this.ClearUnreachableNodesWithVInfo(vinfo);
		}

		/// <summary>
		/// Remove any nodes that are not reachable from the root set in this graph and compact the remaining nodes. 
		/// </summary>
		private void ClearUnreachableNodesWithVInfo(VisitInfo[] vinfo)
		{
			List<ALocation> roots = new List<ALocation>();
			this.FillRootSet(roots, null);
			this.DoDFS(roots, null, vinfo);

			HashSet<int> deadaddr = new HashSet<int>();
			Dictionary<int, int> addrmap = new Dictionary<int, int>(this.m_memory.Count);
			int pushbackloc = 0;
			for(int i = 0; i < this.m_memory.Count; ++i)
			{
				bool nodedead = (vinfo[i].Color == VisitColor.White);
				if(nodedead)
					deadaddr.Add(i);
				else
				{
					addrmap.Add(i, pushbackloc);
					++pushbackloc;
				}
			}

			this.m_memory.RemoveAll((ALocation l) => vinfo[l.Address].Color == VisitColor.White);
			for(int i = 0; i < this.m_memory.Count; ++i)
			{
				this.m_memory[i].DeletePossibleTargets(deadaddr);
				this.m_memory[i].MoveWithUpdatedAddress_ISOMapping(addrmap);
			}

			////
			//Remap all the root info

			List<IRRootIdentifier> rridl = new List<IRRootIdentifier>(this.m_nametonodemap.Keys);
			for(int i = 0; i < rridl.Count; ++i)
				this.m_nametonodemap[rridl[i]] = addrmap[this.m_nametonodemap[rridl[i]]];

			foreach(int[] extt in this.m_externalrefs.Values)
			{
				for(int j = 0; j < extt.Length; ++j)
					extt[j] = addrmap[extt[j]];
			}

			for(int i = 0; i < this.m_evalstack.Count; ++i)
			{
				AEvalStackEntry wdel = this.m_evalstack[i].DeletePossibleTargets(deadaddr);
				this.m_evalstack[i] = wdel.UpdateAddresses_ISOMapping(addrmap);
			}
		}

		/////////////////////////////////////////////////////////
		//Sanity Checking

		/// <summary>
		/// Big check operations, make sure the graph is in a consistent state. Call whenever you feel like it.
		/// </summary>
		[Pure]
		public void CheckConsistent()
		{
#if DEBUG
			if(this.IsInfeasable)
				return;

			if((new HashSet<ALocation>(this.m_memory)).Count != this.m_memory.Count)
				DebugReport.ReportError("Not cool!");

			HashSet<AHomeLocation> seenhomelocs = new HashSet<AHomeLocation>();
			foreach(KeyValuePair<IRRootIdentifier, int> tt in this.m_nametonodemap)
			{
				if(tt.Value < 0 || this.m_memory.Count < tt.Value)
					DebugReport.ReportError("Index out of bounds");

				ALocation mloc = this.m_memory[tt.Value];

				if(!(mloc is AHomeLocation))
					DebugReport.ReportError("Not a home loc!!!");

				if(seenhomelocs.Contains((AHomeLocation)mloc))
					DebugReport.ReportError("We are aliasing!!");
				seenhomelocs.Add((AHomeLocation) mloc);
			}

			foreach(KeyValuePair<AExternalRef, int[]> tt in this.m_externalrefs)
			{
				for(int i = 0; i < tt.Value.Length; ++i)
				{
					if(tt.Value[i] < 0 || this.m_memory.Count < tt.Value[i])
						DebugReport.ReportError("Index out of bounds");
				}
			}

			for(int j = 0; j < this.m_evalstack.Count; ++j)
			{
				AEvalStackEntry nn = this.m_evalstack[j];

				nn.CheckNodeOK(this.m_memory);
			}

			//check each node
			foreach(ALocation nn in this.m_memory)
			{
				//check the node internally
				nn.CheckNodeOK(this.m_memory);
			}
#endif
		}

		/////////////////////////////////////////////////////////
		//Normalize and Merge Routines

		/// <summary>
		/// Normalize routine.
		/// </summary>
		internal void NormalizeLocalFlow(bool cleanfreshdead)
		{ this.NormalizeHelper(false, false, cleanfreshdead); }

		internal void NormalizeAtSimpleCallEntry()
		{ this.NormalizeHelper(false, true, false); }

		internal void NormalizeAtSimpleCallExit()
		{ this.NormalizeHelper(false, false, true); }

		internal void NormalizeAtRecursiveCallEntry()
		{ this.NormalizeHelper(true, true, false); }

		internal void NormalizeAtRecursiveCallExit()
		{ this.NormalizeHelper(true, false, true); }

		private void NormalizeHelper(bool ignoreidentitystate, bool assumecpmustalias, bool cleanfreshdead)
		{
			Contract.Requires(!this.IsInfeasable);

			this.CheckConsistent();

			/////////////////
			//First make sure things are not fugly byt cleaning dead escaping memory and eliminating any unreachable nodes
			this.ClearUnreachableNodesWithVInfo(new VisitInfo[this.m_memory.Count]);

			if(cleanfreshdead)
			{
				bool maybemoredead = this.CleanDeadObjects();
				if(maybemoredead)
					this.ClearUnreachableNodesWithVInfo(new VisitInfo[this.m_memory.Count]);
			}

			////
			//initialize the equivalence partition
			AMemEqPartition eqpart = new AMemEqPartition(this);
			for(int i = 0; i < this.m_memory.Count; ++i)
				eqpart.AddEquivClassForLocation(this.m_memory[i]);
			
			this.ComputePredecessorInfo(eqpart);

			////
			//Fill all the sets of targets related to vars/statics/externals/eval stack
			Dictionary<IRRootIdentifier, List<ALocation>> varandstaticnametargetmap = new Dictionary<IRRootIdentifier, List<ALocation>>();
			Dictionary<AExternalRef, List<ALocation>> externalrefsetmap = new Dictionary<AExternalRef, List<ALocation>>();

			List<Tuple<IRBasicAccessPath, ALocation>>[] evalstackedgesets = new List<Tuple<IRBasicAccessPath, ALocation>>[this.m_evalstack.Count];
			for(int i = 0; i < this.m_evalstack.Count; ++i)
				evalstackedgesets[i] = new List<Tuple<IRBasicAccessPath, ALocation>>();

			this.FillRootTargetInfo(evalstackedgesets, varandstaticnametargetmap, externalrefsetmap);

			List<ALocation> allroots = new List<ALocation>();
			HashSet<AHomeLocation> statichomelocs = new HashSet<AHomeLocation>();
			this.FillRootSet(allroots, statichomelocs);

			////
			//Do the closure of the equiv relations on the rest of the heap structure
			eqpart.ComputeCongruenceClosure(evalstackedgesets, varandstaticnametargetmap, externalrefsetmap, allroots, statichomelocs, ignoreidentitystate);

			////
			//collapse the nodes and remap this based on the resulting eqclass in the partition
			List<List<ALocation>> parts = new List<List<ALocation>>();
			Dictionary<int, int> nodetonewidmap = new Dictionary<int, int>();
			foreach(KeyValuePair<int, AMemPartEqClass> kvp in eqpart.PartIDToEqClassMap)
			{
				if(kvp.Value.PartitionTypes.Count == 1)
				{
					for(int i = 0; i < kvp.Value.PartitionElems.Count; ++i)
						nodetonewidmap.Add(kvp.Value.PartitionElems[i].Address, parts.Count);
					parts.Add(kvp.Value.PartitionElems);
				}
				else
				{
					for(int j = 0; j < kvp.Value.PartitionTypes.Count; ++j)
					{
						IRType currt = kvp.Value.PartitionTypes[j];
						List<ALocation> stp = new List<ALocation>();

						for(int i = 0; i < kvp.Value.PartitionElems.Count; ++i)
						{
							ALocation ll = kvp.Value.PartitionElems[i];
							if(ll.LocationType == currt)
							{
								nodetonewidmap.Add(ll.Address, parts.Count);
								stp.Add(ll);
							}
						}

						parts.Add(stp);
					}
				}
			}

			List<ALocation> newmem = new List<ALocation>();
			for(int i = 0; i < parts.Count; ++i)
			{
				if(parts[i].Count == 1)
				{
					ALocation movei = parts[i][0];
					movei.MoveWithUpdatedAddresses_MayMergeButNoNewInj(nodetonewidmap);
					newmem.Add(movei);
				}
				else
				{
					ALocation mloc = ALocation.JoinLocationSetFromSameContext(parts[i], i, nodetonewidmap);
					newmem.Add(mloc);
				}
			}

			this.m_memory.RemoveRange(newmem.Count, this.m_memory.Count - newmem.Count);
			for(int i = 0; i < newmem.Count; ++i)
				this.m_memory[i] = newmem[i];

			//Update the variable targets
			IRRootIdentifier[] allnamedrefs = new IRRootIdentifier[this.m_nametonodemap.Count];
			this.m_nametonodemap.Keys.CopyTo(allnamedrefs, 0);
			for(int i = 0; i < allnamedrefs.Length; ++i)
			{
				IRRootIdentifier rr = allnamedrefs[i];
				this.m_nametonodemap[rr] = nodetonewidmap[this.m_nametonodemap[rr]];
			}

			//update the external refs
			AExternalRef[] allexternalrefs = new AExternalRef[this.m_externalrefs.Count];
			this.m_externalrefs.Keys.CopyTo(allexternalrefs, 0);
			for(int i = 0; i < allexternalrefs.Length; ++i)
			{
				AExternalRef extr = allexternalrefs[i];
				int[] extrtt = this.m_externalrefs[extr];
				HashSet<int> llt = new HashSet<int>();
				for(int j = 0; j < extrtt.Length; ++j)
					llt.Add(nodetonewidmap[extrtt[j]]);

				this.m_externalrefs[extr] = new int[llt.Count];
				llt.CopyTo(this.m_externalrefs[extr]);
			}

			////
			//Finally update the eval stack and external refs (note we never join fixed locations so no copies are ever created for them).
			for(int i = 0; i < this.m_evalstack.Count; ++i)
			{
				AEvalStackEntry esn = this.m_evalstack[i];
				this.m_evalstack[i] = esn.UpdatedAddresses_MayMergeButNoNewInj(nodetonewidmap);
			}

			this.Focus(assumecpmustalias);

			this.CheckConsistent();
		}

		/// <summary>
		/// We may have nodes which at some point represented newly allocated objects but can no longer do so (specifically 
		/// there are no predecessor objects which have had pointer fields updated in this method body). Here we are going 
		/// to clean all of this info out.
		/// </summary>
		private bool CleanDeadObjects()
		{
			HashSet<ALocation> evalrefed = new HashSet<ALocation>();
			Dictionary<AObject, List<ALocation>> predmap = new Dictionary<AObject, List<ALocation>>();

			for(int i = 0; i < this.m_evalstack.Count; ++i)
			{
				IEnumerator<ATrgtEnum> trgtenum1 = this.m_evalstack[i].GetATrgtEnumerator();
				while(trgtenum1.MoveNext())
				{
					ATrgtEnum tte1 = trgtenum1.Current;
					ALocation ll1 = this.ResolveRawAddress(tte1.TrgtAddress);
					evalrefed.Add(ll1);
				}
			}

			for(int i = 0; i < this.m_memory.Count; ++i)
			{
				ALocation ll2 = this.m_memory[i];

				if(evalrefed.Contains(ll2))
						continue;

				if(ll2 is AObject && ll2.MayBeInternalAlloc())
					predmap.Add((AObject)ll2, new List<ALocation>());
			}

			for(int i = 0; i < this.m_memory.Count; ++i)
			{
				ALocation ll3 = this.m_memory[i];
				IEnumerator<ATrgtEnum> trgtenum = ll3.GetTargetEnum();
				while(trgtenum.MoveNext())
				{
					ATrgtEnum tte3 = trgtenum.Current;
					ALocation tl3 = this.ResolveRawAddress(tte3.TrgtAddress);

					if(tl3 is AObject && predmap.ContainsKey((AObject)tl3))
						predmap[(AObject)tl3].Add(ll3);
				}
			}

			//find any objects that have some escaping objects but that are preceeded by objects which do not have modifications 
			//to fields which might contain pointers to the objects in ao
			Queue<AObject> toproc = new Queue<AObject>();
			foreach(KeyValuePair<AObject, List<ALocation>> pao in predmap)
			{
				bool onlynonupdatedpred = true;
				for(int i = 0; i < pao.Value.Count; ++i)
				{
					ALocation llp = pao.Value[i];
					onlynonupdatedpred &= (!UseModInfo.HasLocationOfPtrOrRefTypeBeenModifiedInCall(llp.LocationType, llp.UMInfo));
				}

				if(onlynonupdatedpred)
					toproc.Enqueue(pao.Key);
			}

			bool edgeelim = false;
			while(toproc.Count != 0)
			{
				AObject ao = toproc.Dequeue();
				
				bool onlynonupdatedpred = true;
				List<ALocation> predlocs = predmap[ao];
				for(int i = 0; i < predlocs.Count; ++i)
				{
					ALocation llf = predlocs[i];
					bool notmod = !UseModInfo.HasLocationOfPtrOrRefTypeBeenModifiedInCall(llf.LocationType, llf.UMInfo);
					onlynonupdatedpred &= notmod;

					IEnumerator<ATrgtEnum> ftrgtenum = llf.GetTargetEnum();
					while(ftrgtenum.MoveNext())
					{
						ATrgtEnum ftte = ftrgtenum.Current;
						if(ftte.TrgtAddress != ao.Address)
							continue;

						//we can just eliminate the edge entirely since it can only have been assigned internally and we see no assignement!
						if(notmod & ao.MustBeInternalAlloc())
						{
							Contract.Assert(llf is AObject, "Fixed locations are always mod so??");
							((AObject)llf).ScrubInfeasibleRef(ftte);
							edgeelim = true;
						}
					}
				}

				if(onlynonupdatedpred)
				{
					IEnumerator<ATrgtEnum> trgtenumc = ao.GetTargetEnum();
					while(trgtenumc.MoveNext())
					{
						AObject lltc = (AObject)this.ResolveRawAddress(trgtenumc.Current.TrgtAddress);
						if(predmap.ContainsKey(lltc))
							toproc.Enqueue(lltc);
					}

					//we can just eliminate any internal escape and internal use/mod info
					edgeelim |= ao.ElimFreshAllocData();
				} 
			}

			return edgeelim;
		}

		/// <summary>
		/// If a node represents a single location then we can mark the outgoing (non-collection) abstract pointers as Injective
		/// </summary>
		private void Focus(bool assumecpmustalias)
		{
			short[] predcount = new short[this.m_memory.Count];
			
			for(int i = 0; i < this.m_evalstack.Count; ++i)
			{
				IEnumerator<ATrgtEnum> trgtenum = this.m_evalstack[i].GetATrgtEnumerator();
				while(trgtenum.MoveNext())
				{
					ATrgtEnum tte = trgtenum.Current;
					ALocation l = this.ResolveRawAddress(tte.TrgtAddress);
					predcount[l.Address]++;
				}
			}

			if(!assumecpmustalias)
			{
				foreach(int[] cpta in this.m_externalrefs.Values)
				{
					for(int j = 0; j < cpta.Length; ++j)
						predcount[cpta[j]]++;
				}
			}

			for(int i = 0; i < this.m_memory.Count; ++i)
			{
				IEnumerator<ATrgtEnum> trgtenum = this.m_memory[i].GetTargetEnum();
				while(trgtenum.MoveNext())
				{
					ATrgtEnum tte = trgtenum.Current;
					ALocation l = this.ResolveRawAddress(tte.TrgtAddress);
					predcount[l.Address]++;
				}
			}

			Queue<ALocation> wlq = new Queue<ALocation>();

			for(int i = 0; i < this.m_evalstack.Count; ++i)
			{
				IEnumerator<ATrgtEnum> trgtenum = this.m_evalstack[i].GetATrgtEnumerator();
				while(trgtenum.MoveNext())
				{
					ATrgtEnum tte = trgtenum.Current;
					ALocation l = this.ResolveRawAddress(tte.TrgtAddress);
					if((!l.IsUniqueLocation()) & (predcount[l.Address] == 1))
						l.UpdateAsUniqueLocation();
				}
			}

			for(int i = 0; i < this.m_memory.Count; ++i)
			{
				if(this.m_memory[i].IsUniqueLocation())
					wlq.Enqueue(this.m_memory[i]);
			}

			while(wlq.Count != 0)
			{
				ALocation l = wlq.Dequeue();
				
				IEnumerator<ATrgtEnum> trgtenum = l.GetTargetEnum();
				while(trgtenum.MoveNext())
				{
					ATrgtEnum tte = trgtenum.Current;
					ALocation sl = this.ResolveRawAddress(tte.TrgtAddress);
					if(tte.BAPPath.AccessPathHasSummaryLocation | (predcount[sl.Address] != 1))
						continue;

					if(!sl.IsUniqueLocation())
					{
						sl.UpdateAsUniqueLocation();
						wlq.Enqueue(sl);
					}
				}
			}
		}

		/// <summary>
		/// This this is used for joining 2 models from the same local flow context (e.g. we know they have the same id and external ref name sets).
		/// </summary>
		internal static AProgramMemory PMemoryMergeLocalFlow(AProgramMemory m1, AProgramMemory m2, bool onlym1stack)
		{
			Contract.Requires(m1 != null && (!m1.IsInfeasable));
			Contract.Requires(m2 != null && (!m2.IsInfeasable));
			Contract.Ensures(Contract.Result<AProgramMemory>() != null);

			Tuple<AMemEqPartition, AProgramMemory> pmcs = AProgramMemory.PMemoryMergeHelper(m1, m2, false, false, onlym1stack);
			return pmcs.Item2;
		}

		/// <summary>
		/// This this is used for computing the merge partition for 2 models at call entry.
		/// </summary>
		internal static AMemEqPartition PMemoryMergeCallsPartition(AProgramMemory m1, AProgramMemory m2)
		{
			return AProgramMemory.PMemoryMergeHelper(m1, m2, true, true, false).Item1;
		}

		/// <summary>
		/// This this is used for joining 2 models at call entry.
		/// </summary>
		internal static AProgramMemory PMemoryMergeCallsEntry(AProgramMemory m1, AProgramMemory m2)
		{
			Contract.Requires(m1 != null && (!m1.IsInfeasable));
			Contract.Requires(m2 != null && (!m2.IsInfeasable));
			Contract.Ensures(Contract.Result<AProgramMemory>() != null);

			Tuple<AMemEqPartition, AProgramMemory> pmcs = AProgramMemory.PMemoryMergeHelper(m1, m2, true, false, false);
			return pmcs.Item2;
		}

		internal static Tuple<AMemEqPartition, AProgramMemory> PMemoryMergeHelper(AProgramMemory m1, AProgramMemory m2, bool ignoreidentitystate, bool nobuild, bool onlym1stack)
		{
			Contract.Assert(m1.m_nametonodemap.Count >= m2.m_nametonodemap.Count);
			Contract.Assert(m1.m_evalstack.Count == m2.m_evalstack.Count);

			/////////////////
			//First make sure things are not fugly
			VisitInfo[] vinfo1 = new VisitInfo[m1.m_memory.Count]; //we use this later too
			m1.DoDFS(vinfo1);

			VisitInfo[] vinfo2 = new VisitInfo[m2.m_memory.Count]; //we use this later too
			m2.DoDFS(vinfo2);

			////
			//initialize the equivalence partition
			AMemEqPartition eqpart = new AMemEqPartition(m1, m2);

			for(int i = 0; i < m1.m_memory.Count; ++i)
			{
				ALocation ll = m1.m_memory[i];
				eqpart.AddEquivClassForLocation(ll);
			}

			for(int i = 0; i < m2.m_memory.Count; ++i)
			{
				ALocation ll = m2.m_memory[i];
				eqpart.AddEquivClassForLocation(ll);
			}

			m1.ComputePredecessorInfo(eqpart);
			m2.ComputePredecessorInfo(eqpart);

			////
			//Do all the fixed root set normalization
			Dictionary<IRRootIdentifier, List<ALocation>> varandstaticnametargetmap = new Dictionary<IRRootIdentifier, List<ALocation>>();
			Dictionary<AExternalRef, List<ALocation>> externalrefsetmap = new Dictionary<AExternalRef, List<ALocation>>();

			Contract.Assert(m1.m_evalstack.Count == m2.m_evalstack.Count);
			List<Tuple<IRBasicAccessPath, ALocation>>[] evalstackedgesets = new List<Tuple<IRBasicAccessPath, ALocation>>[m1.m_evalstack.Count];
			for(int i = 0; i < m1.m_evalstack.Count; ++i)
				evalstackedgesets[i] = new List<Tuple<IRBasicAccessPath, ALocation>>();

			m1.FillRootTargetInfo(evalstackedgesets, varandstaticnametargetmap, externalrefsetmap);
			m2.FillRootTargetInfo(evalstackedgesets, varandstaticnametargetmap, externalrefsetmap);

			List<ALocation> allroots = new List<ALocation>();
			HashSet<AHomeLocation> statichomelocs = new HashSet<AHomeLocation>();
			m1.FillRootSet(allroots, statichomelocs);
			m2.FillRootSet(allroots, statichomelocs);

			////
			//Do the closure of the equiv relations on the rest of the heap structure
			eqpart.ComputeCongruenceClosure(evalstackedgesets, varandstaticnametargetmap, externalrefsetmap, allroots, statichomelocs, ignoreidentitystate);

			AProgramMemory respm = nobuild ? null : BuildModelFromEquivClosureAndMBuild(eqpart, m1, vinfo1, m2, vinfo2, onlym1stack);

			return new Tuple<AMemEqPartition, AProgramMemory>(eqpart, respm);
		}

		/////////////////////////
		//Support for Normalize and Merge Routines

		/// <summary>
		/// Given a equivalence class in look at the locations and split them into the set of locations that came from <c>m1</c> and the 
		/// set that came from <c>m2</c>, put the locations in the respective collections.
		/// </summary>
		private static void ExtractNodesFromPartitionBasedOnSource(AMemPartEqClass eqclass, IRType oftype, AProgramMemory m1, List<ALocation> from1, AProgramMemory m2, List<ALocation> from2)
		{
			Contract.Requires(eqclass != null);
			Contract.Requires(oftype != null);
			Contract.Requires(m1 != null && (!m1.IsInfeasable));
			Contract.Requires(from1 != null && from1.Count == 0);
			Contract.Requires(m2 != null && (!m2.IsInfeasable));
			Contract.Requires(from2 != null && from2.Count == 0);
			Contract.Requires(from1 != from2);

			for(int i = 0; i < eqclass.PartitionElems.Count; ++i)
			{
				ALocation ll = eqclass.PartitionElems[i];
				Contract.Assert((ll.Address < m1.m_memory.Count && ll == m1.m_memory[ll.Address]) || (ll.Address < m2.m_memory.Count && ll == m2.m_memory[ll.Address]));

				if(ll.LocationType == oftype)
				{
					if(ll.Address < m1.m_memory.Count && ll == m1.m_memory[ll.Address]) //then it is from m1
						from1.Add(ll);
					else
						from2.Add(ll);
				}
			}
		}

		/// <summary>
		/// Given a closed equivalence relation and 2 models that were merged to create it, compute and return the abstract memory that represents the closure structure/info.
		/// Assumes that the nameset in <c>m1</c> is either equal to or we know subsumes the nameset in <c>m2</c>.
		/// </summary>
		internal static AProgramMemory BuildModelFromEquivClosureAndMBuild(AMemEqPartition eqpart, AProgramMemory m1, VisitInfo[] vinfo1, AProgramMemory m2, VisitInfo[] vinfo2, bool onlym1stack)
		{
			Contract.Requires(eqpart != null);
			Contract.Requires(m1 != null && (!m1.IsInfeasable));
			Contract.Requires(vinfo1 != null);
			Contract.Requires(m2 != null && (!m2.IsInfeasable));
			Contract.Requires(vinfo2 != null);
			Contract.Ensures(Contract.Result<AProgramMemory>() != null);

			Contract.Assert(m1.m_memory.Count == vinfo1.Length);
			Contract.Assert(m2.m_memory.Count == vinfo2.Length);

			AProgramMemory resmodel = new AProgramMemory();

			////
			//collapse the nodes and remap this based on the resulting eqclass in the partition
			Dictionary<int, int> loctonewidmap1 = new Dictionary<int, int>();
			Dictionary<int, int> loctonewidmap2 = new Dictionary<int, int>();
			AMemPartEqClass[] parts = eqpart.FillNodeIDToEquivIDMappingAndArray(m1, loctonewidmap1, m2, loctonewidmap2); //this is wild watch it and what happens below

			List<ALocation> tmergefrom1 = new List<ALocation>();
			List<ALocation> tmergefrom2 = new List<ALocation>();
			for(int i = 0; i < parts.Length; ++i)
			{
				for(int j = 0; j < parts[i].PartitionTypes.Count; ++j)
				{
					tmergefrom1.Clear();
					tmergefrom2.Clear();
					AProgramMemory.ExtractNodesFromPartitionBasedOnSource(parts[i], parts[i].PartitionTypes[j], m1, tmergefrom1, m2, tmergefrom2);

					if((tmergefrom1.Count == 1) & (tmergefrom2.Count == 0))
					{
						ALocation movei = tmergefrom1[0].CopyLocation();
						movei.MoveWithUpdatedAddresses_MayMergeButNoNewInj(loctonewidmap1);
						resmodel.m_memory.Add(movei);
					}
					else if((tmergefrom1.Count == 0) & (tmergefrom2.Count == 1))
					{
						ALocation movei = tmergefrom2[0].CopyLocation();
						movei.MoveWithUpdatedAddresses_MayMergeButNoNewInj(loctonewidmap2);
						resmodel.m_memory.Add(movei);
					}
					else
					{
						ALocation res1 = null;
						if(tmergefrom1.Count != 0)
						{
							if(tmergefrom1.Count == 1)
							{
								IEnumerator<ALocation> ll1e = tmergefrom1.GetEnumerator();
								ll1e.MoveNext();
								res1 = ll1e.Current.CopyLocation();
								res1.MoveWithUpdatedAddresses_MayMergeButNoNewInj(loctonewidmap1);
							}
							else
								res1 = ALocation.JoinLocationSetFromSameContext(tmergefrom1, resmodel.m_memory.Count, loctonewidmap1);
						}

						ALocation res2 = null;
						if(tmergefrom2.Count != 0)
						{
							if(tmergefrom2.Count == 1)
							{
								IEnumerator<ALocation> ll2e = tmergefrom2.GetEnumerator();
								ll2e.MoveNext();
								res2 = ll2e.Current.CopyLocation();
								res2.MoveWithUpdatedAddresses_MayMergeButNoNewInj(loctonewidmap2);
							}
							else
								res2 = ALocation.JoinLocationSetFromSameContext(tmergefrom2, resmodel.m_memory.Count, loctonewidmap2);
						}

						ALocation mergenl;
						if((res1 != null) & (res2 != null))
							mergenl = ALocation.JoinLocationsFromDifferentContexts(res1, res2);
						else if(res1 != null)
							mergenl = res1;
						else
							mergenl = res2;


						resmodel.m_memory.Add(mergenl);
					}
				}
			}

			//Update the variable targets
			IRRootIdentifier[] allnamedrefs = new IRRootIdentifier[m1.m_nametonodemap.Count]; //m1 should always be a superset of m2
			m1.m_nametonodemap.Keys.CopyTo(allnamedrefs, 0);
			for(int i = 0; i < allnamedrefs.Length; ++i)
			{
				IRRootIdentifier rr = allnamedrefs[i];
				resmodel.m_nametonodemap.Add(rr, loctonewidmap1[m1.m_nametonodemap[rr]]);
			}

			//update the external refs
			HashSet<AExternalRef> allextr = new HashSet<AExternalRef>();
			allextr.UnionWith(m1.m_externalrefs.Keys);
			allextr.UnionWith(m2.m_externalrefs.Keys);
			foreach(AExternalRef extr in allextr)
			{
				HashSet<int> llt = new HashSet<int>();

				if(m1.m_externalrefs.ContainsKey(extr))
				{
					int[] extrttbm = m1.m_externalrefs[extr];
					for(int j = 0; j < extrttbm.Length; ++j)
						llt.Add(loctonewidmap1[extrttbm[j]]);
				}

				if(m2.m_externalrefs.ContainsKey(extr))
				{
					int[] extrttom = m2.m_externalrefs[extr];
					for(int j = 0; j < extrttom.Length; ++j)
						llt.Add(loctonewidmap2[extrttom[j]]);
				}

				int[] ftrgta = new int[llt.Count];
				llt.CopyTo(ftrgta);
				resmodel.m_externalrefs.Add(extr, ftrgta);
			}

			////
			//Finally update the eval stack and external refs (note we never join fixed locations so no copies are ever created for them).
			for(int i = 0; i < m1.m_evalstack.Count; ++i) //again should be the same for m1 and m2
			{
				AEvalStackEntry sn1 = m1.m_evalstack[i].UpdatedAddresses_MayMergeButNoNewInj(loctonewidmap1);
				AEvalStackEntry sn2 = m2.m_evalstack[i].UpdatedAddresses_MayMergeButNoNewInj(loctonewidmap2);
				AEvalStackEntry esn;

				if(onlym1stack)
					esn = sn1;
				else
					esn = sn1.JoinEvalStackEntries(sn2);
				
				resmodel.m_evalstack.Add(esn);
			}

			return resmodel;
		}

		/// <summary>
		/// Place all the var/static/external/eval stack info into the given dictionaries.
		/// </summary>
		private void FillRootTargetInfo(List<Tuple<IRBasicAccessPath, ALocation>>[] evalstackedgemap, Dictionary<IRRootIdentifier, List<ALocation>> varandstaticnametargetmap, Dictionary<AExternalRef, List<ALocation>> externalrefmap)
		{
			for(int i = 0; i < this.m_evalstack.Count; ++i)
			{
				IEnumerator<ATrgtEnum> trgtenum = this.m_evalstack[i].GetATrgtEnumerator();
				while(trgtenum.MoveNext())
				{
					ATrgtEnum te = trgtenum.Current;
					ALocation tn = this.m_memory[te.TrgtAddress];
					evalstackedgemap[i].Add(new Tuple<IRBasicAccessPath, ALocation>(te.BAPPath, tn));
				}
			}

			//first compute home locs
			foreach(KeyValuePair<IRRootIdentifier, int> rr in this.m_nametonodemap)
			{
				ALocation tl = this.m_memory[rr.Value];
				if(!varandstaticnametargetmap.ContainsKey(rr.Key))
					varandstaticnametargetmap.Add(rr.Key, new List<ALocation>());

				varandstaticnametargetmap[rr.Key].Add(tl);
			}

			foreach(KeyValuePair<AExternalRef, int[]> extr in this.m_externalrefs)
			{
				if(!externalrefmap.ContainsKey(extr.Key))
					externalrefmap.Add(extr.Key, new List<ALocation>());

				for(int j = 0; j < extr.Value.Length; ++j)
				{
					ALocation tn = this.m_memory[extr.Value[j]];
					externalrefmap[extr.Key].Add(tn);
				}
			}
		}

		private void ComputePredecessorInfo(AMemEqPartition neq)
		{
			HashSet<ALocation> homelocs = new HashSet<ALocation>();

			foreach(KeyValuePair<IRRootIdentifier, int> rr in this.m_nametonodemap)
			{
				AHomeLocation ll = (AHomeLocation)this.m_memory[rr.Value];
				neq.SetAsNameHomeLocation(rr.Key, ll);

				homelocs.Add(ll);
				IEnumerator<ATrgtEnum> trgtenum = ll.GetTargetEnum();
				while(trgtenum.MoveNext())
				{
					ATrgtEnum tee = trgtenum.Current;
					ALocation tl = this.m_memory[tee.TrgtAddress];
					neq.AddAsTargetOfVarOrStatic(rr.Key, tl);
				}
			}

			foreach(KeyValuePair<AExternalRef, int[]> extr in this.m_externalrefs)
			{
				for(int j = 0; j < extr.Value.Length; ++j)
				{
					ALocation tl = this.m_memory[extr.Value[j]];
					neq.AddAsTargetOfExternalRef(extr.Key, tl);
				}
			}

			for(int i = 0; i < this.m_evalstack.Count; ++i)
			{
				if(this.m_evalstack[i].SLocType is IRPrimitiveType)
					continue;

				IEnumerator<ATrgtEnum> trgtenum = this.m_evalstack[i].GetATrgtEnumerator();
				while(trgtenum.MoveNext())
				{
					ATrgtEnum tee = trgtenum.Current;
					ALocation tl = this.m_memory[tee.TrgtAddress];
					neq.AddAsTargetOfStackLoc(i, tee.BAPPath, tl);
				}
			}

			for(int i = 0; i < this.m_memory.Count; ++i)
			{
				ALocation ll = this.m_memory[i];
				if(homelocs.Contains(ll))
					continue;

				IEnumerator<ATrgtEnum> trgtenum = ll.GetTargetEnum();
				while(trgtenum.MoveNext())
				{
					ATrgtEnum tee = trgtenum.Current;
					ALocation tl = this.m_memory[tee.TrgtAddress];

					//we are not interested in self edges here to we exclude them
					if(ll.Address != tee.TrgtAddress)
						neq.AddMemorySuccessorAndPredecessor(ll, tee.BAPPath, tl);
				}
			}
		}

		/////////////////////////////////////////////////////////
		//Compare Routines
		//We construct the graphs such that the compare routine can, at each step of matching, find at least one target in the unmatched frontier 
		//that has a unique match (or if there is no match then we know that the graphs are not equal).

		/// <summary>
		/// Find all the possible matches for <c>forref</c> in the reference <c>pr2</c> and place them in <c>into</c>.
		/// </summary>
		private static void FindPossibleMatchesForReferenceInStack(int spos, APossibleReferenceTarget forref, ALocation fortrgt, List<ATrgtEnum> into, AMemCompareStruct comps, AReference pr2, AProgramMemory m2)
		{
			IEnumerator<ATrgtEnum> trgtenum = pr2.GetATrgtEnumerator();
			while(trgtenum.MoveNext())
			{
				ATrgtEnum tte = trgtenum.Current;
				APossibleReferenceTarget r2 = pr2.ResolveRefFromEnum(tte);
				ALocation tl2 = m2.ResolveReferenceTarget(r2);

				//check if the target offsets or nullity are inconsistent
				if(!forref.DomainEqualIgnoreTargetAddress(r2))
					continue;

				//check if we have already mapped r2, if it would create a conflict in node targets, or is totally inconsistent
				Tuple<int, ATrgtEnum> matchin2 = new Tuple<int, ATrgtEnum>(spos, tte);
				if(comps.StackTargetMatchDoneInM2.Contains(matchin2) || (comps.AddressMap.ContainsKey(fortrgt.Address) && comps.AddressMap[fortrgt.Address] != tl2.Address))
					continue;

				//if we get here then matching is consistent, so use edge/node check functions
				bool locsaequiv = ALocation.EqualALocation(fortrgt, tl2, comps.CompareStyle == AMemCompareStruct.CompareTag.CallEntry, comps.CompareStyle == AMemCompareStruct.CompareTag.CallExit);
				if(!locsaequiv)
					continue;

				//otherwise the match is ok, and left in the vector
				into.Add(tte);
			}
		}

		/// <summary>
		/// Find all the possible matches for <c>forptr</c> in the ponterset <c>pr2</c> and place them in <c>into</c>.
		/// </summary>
		private static void FindPossibleMatchesForPointerInStack(int spos, APossiblePointerTarget forptr, ALocation fortrgt, List<ATrgtEnum> into, AMemCompareStruct comps, APtrValueMap pr2, AProgramMemory m2)
		{
			IEnumerator<ATrgtEnum> trgtenum = pr2.GetATrgtEnumerator();
			while(trgtenum.MoveNext())
			{
				ATrgtEnum tte = trgtenum.Current;
				APossiblePointerTarget p2 = pr2.ResolvePtrFromEnum(tte);
				ALocation tl2 = m2.ResolvePointerTarget(p2);

				//check if the pointer informatino is inconsistent
				bool ptrinfook = forptr.DomainEqualIgnoreTargetAddress(p2);
				if(!ptrinfook)
					continue;

				//check if we have already mapped r2, if it would create a conflict in node targets, or is totally inconsistent
				Tuple<int, ATrgtEnum> matchin2 = new Tuple<int, ATrgtEnum>(spos, tte);
				if(comps.StackTargetMatchDoneInM2.Contains(matchin2) || (comps.AddressMap.ContainsKey(fortrgt.Address) && comps.AddressMap[fortrgt.Address] != tl2.Address))
					continue;

				//if we get here then matching is consistent, so use edge/node check functions
				bool locsaequiv = ALocation.EqualALocation(fortrgt, tl2, comps.CompareStyle == AMemCompareStruct.CompareTag.CallEntry, comps.CompareStyle == AMemCompareStruct.CompareTag.CallExit);
				if(!locsaequiv)
					continue;

				//otherwise the match is ok, and left in the vector
				into.Add(tte);
			}
		}

		/// <summary>
		/// Find all the possible matches for <c>forref</c> in the reference <c>pr2</c> and place them in <c>into</c>.
		/// </summary>
		private static void FindPossibleMatchesForReferenceInLocation(ALocation lpos, APossibleReferenceTarget forref, ALocation fortrgt, List<ATrgtEnum> into, AMemCompareStruct comps, AReference pr2, AProgramMemory m2)
		{
			IEnumerator<ATrgtEnum> trgtenum = pr2.GetATrgtEnumerator();
			while(trgtenum.MoveNext())
			{
				ATrgtEnum tte = trgtenum.Current;
				APossibleReferenceTarget r2 = pr2.ResolveRefFromEnum(tte);
				ALocation tl2 = m2.ResolveReferenceTarget(r2);

				//check if the target offsets are inconsistent
				if(!forref.DomainEqualIgnoreTargetAddress(r2))
					continue;

				//check if we have already mapped r2, if it would create a conflict in node targets, or is totally inconsistent
				Tuple<ALocation, ATrgtEnum> matchin2 = new Tuple<ALocation, ATrgtEnum>(lpos, tte);
				if(comps.LocationTargetMatchDoneInM2.Contains(matchin2) || (comps.AddressMap.ContainsKey(fortrgt.Address) && comps.AddressMap[fortrgt.Address] != tl2.Address))
					continue;

				//if we get here then matching is consistent, so use edge/node check functions
				bool locsaequiv = ALocation.EqualALocation(fortrgt, tl2, comps.CompareStyle == AMemCompareStruct.CompareTag.CallEntry, comps.CompareStyle == AMemCompareStruct.CompareTag.CallExit);
				if(!locsaequiv)
					continue;

				//otherwise the match is ok, and left in the vector
				into.Add(tte);
			}
		}

		/// <summary>
		/// Find all the possible matches for <c>forptr</c> in the ponterset <c>pr2</c> and place them in <c>into</c>.
		/// </summary>
		private static void FindPossibleMatchesForPointerInAllocation(ALocation lpos, APossiblePointerTarget forptr, ALocation fortrgt, List<ATrgtEnum> into, AMemCompareStruct comps, APtrValueMap pr2, AProgramMemory m2)
		{
			IEnumerator<ATrgtEnum> trgtenum = pr2.GetATrgtEnumerator();
			while(trgtenum.MoveNext())
			{
				ATrgtEnum tte = trgtenum.Current;
				APossiblePointerTarget p2 = pr2.ResolvePtrFromEnum(tte);
				ALocation tl2 = m2.ResolvePointerTarget(p2);

				//check if the pointer informatino is inconsistent
				if(!forptr.DomainEqualIgnoreTargetAddress(p2))
					continue;

				//check if we have already mapped r2, if it would create a conflict in node targets, or is totally inconsistent
				Tuple<ALocation, ATrgtEnum> matchin2 = new Tuple<ALocation, ATrgtEnum>(lpos, tte);
				if(comps.LocationTargetMatchDoneInM2.Contains(matchin2) || (comps.AddressMap.ContainsKey(fortrgt.Address) && comps.AddressMap[fortrgt.Address] != tl2.Address))
					continue;

				//if we get here then matching is consistent, so use edge/node check functions
				bool locsaequiv = ALocation.EqualALocation(fortrgt, tl2, comps.CompareStyle == AMemCompareStruct.CompareTag.CallEntry, comps.CompareStyle == AMemCompareStruct.CompareTag.CallExit);
				if(!locsaequiv)
					continue;

				//otherwise the match is ok, and left in the vector
				into.Add(tte);
			}
		}

		/// <summary>
		/// If we are matching a target that originates at a call stack location in <c>m1</c> use this to find candidate matches in <c>m2</c>.
		/// </summary>
		private static void FindMatchesForStackLocation(AProgramMemory m1, AProgramMemory m2, int spo1, ATrgtEnum epos1, List<ATrgtEnum> pmatch, AMemCompareStruct comps)
		{
			Contract.Requires(m1 != null && (!m1.IsInfeasable));
			Contract.Requires(m2 != null && (!m2.IsInfeasable));
			Contract.Requires(pmatch != null && pmatch.Count == 0);
			Contract.Requires(comps != null && (comps.CompareStyle != AMemCompareStruct.CompareTag.CallEntry), "Stack should be empty at call entry??");

			if(m1.m_evalstack[spo1].SLocType is IRReferenceType)
			{
				APossibleReferenceTarget r1 = m1.m_evalstack[spo1].ResolveRefFromEnum(epos1);
				ALocation tl1 = m1.ResolveReferenceTarget(r1);

				AProgramMemory.FindPossibleMatchesForReferenceInStack(spo1, r1, tl1, pmatch, comps, m2.m_evalstack[spo1].ReferenceValue, m2);
			}
			else if(m1.m_evalstack[spo1].SLocType is IRPtrType)
			{
				APossiblePointerTarget p1 = m1.m_evalstack[spo1].ResolvePtrFromEnum(epos1);
				ALocation tl1 = m1.ResolvePointerTarget(p1);

				AProgramMemory.FindPossibleMatchesForPointerInStack(spo1, p1, tl1, pmatch, comps, m2.m_evalstack[spo1].PointerValue, m2);
			}
			else if(m1.m_evalstack[spo1].SLocType is IRStructType)
			{
				APossiblePointerTarget p1 = m1.m_evalstack[spo1].ResolvePtrFromEnum(epos1);
				ALocation tl1 = m1.ResolvePointerTarget(p1);

				AProgramMemory.FindPossibleMatchesForPointerInStack(spo1, p1, tl1, pmatch, comps, m2.m_evalstack[spo1].StructValue, m2);
			}
			else
			{ ;}
		}

		/// <summary>
		/// If we are matching an edge that originates at an external ref name <c>m1</c> use this to find candidate matches in <c>m2</c>.
		/// </summary>
		private static void FindMatchesForExternalRefTarget(AProgramMemory m1, AProgramMemory m2, AExternalRef erf, int epos1, List<int> pmatch, AMemCompareStruct comps)
		{
			Contract.Requires(m1 != null && (!m1.IsInfeasable));
			Contract.Requires(m2 != null && (!m2.IsInfeasable));
			Contract.Requires(erf != null && m2.m_externalrefs.ContainsKey(erf), "Names should always be the same");
			Contract.Requires(pmatch != null && pmatch.Count == 0);
			Contract.Requires(comps != null && (comps.CompareStyle != AMemCompareStruct.CompareTag.CallEntry), "Should not be matching ext refs by name at call entry??");

			int n1id = m1.m_externalrefs[erf][epos1];
			ALocation tl1 = m1.ResolveRawAddress(n1id);

			int[] tnl = m2.m_externalrefs[erf];
			for(int i = 0; i < tnl.Length; ++i)
			{
				int n2id = tnl[i];
				ALocation tl2 = m2.ResolveRawAddress(n2id);

				//check if we have already mapped e2, if it would create a conflict in node targets, or is totally inconsistent
				Tuple<AExternalRef, int> matchin2 = new Tuple<AExternalRef, int>(erf, i);
				if(comps.ExtRefTargetMatchDoneInM2.Contains(matchin2) || (comps.AddressMap.ContainsKey(tl1.Address) && comps.AddressMap[tl1.Address] != tl2.Address))
					continue;

				//if we get here then matching is consistent, so use edge/node check functions
				bool locsaequiv = ALocation.EqualALocation(tl1, tl2, false, comps.CompareStyle == AMemCompareStruct.CompareTag.CallExit);
				if(!locsaequiv)
					continue;

				//otherwise the match is ok, and left in the vector
				pmatch.Add(i);
			}
		}

		/// <summary>
		/// If we are matching an edge that originates at an MNode in <c>m1</c> use this to find candidate matches in <c>m2</c>.
		/// </summary>
		private static void FindMatchesForALocation(AProgramMemory m1, AProgramMemory m2, ALocation n1, ATrgtEnum epos1, List<ATrgtEnum> pmatch, AMemCompareStruct comps)
		{
			Contract.Requires(m1 != null && (!m1.IsInfeasable));
			Contract.Requires(m2 != null && (!m2.IsInfeasable));
			Contract.Requires(n1 != null);
			Contract.Requires(pmatch != null && pmatch.Count == 0);
			Contract.Requires(comps != null);

			if(n1.LocationType is IRReferenceType)
			{
				APossibleReferenceTarget r1 = ((AHomeLocation)n1).ResolveRefFromEnum(epos1);
				ALocation tl1 = m1.ResolveReferenceTarget(r1);

				AHomeLocation n2 = (AHomeLocation)m2.ResolveRawAddress(comps.AddressMap[n1.Address]);
				AProgramMemory.FindPossibleMatchesForReferenceInLocation(n2, r1, tl1, pmatch, comps, n2.ReferenceValue, m2);
			}
			else if(n1.LocationType is IRPtrType)
			{
				APossiblePointerTarget p1 = n1.ResolvePtrFromEnum(epos1);
				ALocation tl1 = m1.ResolvePointerTarget(p1);

				AHomeLocation n2 = (AHomeLocation)m2.ResolveRawAddress(comps.AddressMap[n1.Address]);
				AProgramMemory.FindPossibleMatchesForPointerInAllocation(n2, p1, tl1, pmatch, comps, ((AHomeLocation)n2).PointerValue, m2);
			}
			else if(n1.LocationType is IRStructType || n1.LocationType is IRClassType)
			{
				APossiblePointerTarget p1 = n1.ResolvePtrFromEnum(epos1);
				ALocation tl1 = m1.ResolvePointerTarget(p1);

				ALocation n2 = m2.ResolveRawAddress(comps.AddressMap[n1.Address]);
				AProgramMemory.FindPossibleMatchesForPointerInAllocation(n2, p1, tl1, pmatch, comps, n2.StructOrClassPointers, m2);
			}
			else
			{ ;}
		}

		/// <summary>
		/// Keep trying to match edges from the edge frontier until we are out or we fail to find a match. Backtrack as needed.
		/// </summary>
		private static bool GraphCompareDoIt(AProgramMemory m1, AProgramMemory m2, AMemCompareStruct comps)
		{
			if(comps.LocationTargetMatchFrontier.Count == 0 & comps.ExtRefTargetsToMatchFrontier.Count == 0 & comps.StackTargetMatchFrontier.Count == 0)
			{
				if(comps.CompareStyle == AMemCompareStruct.CompareTag.CallEntry)
					return GraphCompareExtRefCallEntry(m1, m2, comps);
				else
					return true;
			}

			/////////
			//select a match & get the associated possible matches

			int typeofmatch; //0 is location, 1 is external, 2 is stack
			int targetaddr; //address that is being matched to in m1
			List<int> extpmatch = new List<int>(); //the matches in m2
			List<ATrgtEnum> pmatch = new List<ATrgtEnum>(); //the matches in m2
			int matchcount = 0;

			Tuple<ALocation, ATrgtEnum> mnpp = null;
			Tuple<AExternalRef, int> erpp = null;
			Tuple<int, ATrgtEnum> evspp = null;

			if(comps.LocationTargetMatchFrontier.Count != 0)
			{
				typeofmatch = 0;
				mnpp = comps.LocationTargetMatchFrontier.First.Value;
				comps.LocationTargetMatchFrontier.RemoveFirst();
				targetaddr = mnpp.Item2.TrgtAddress;
				FindMatchesForALocation(m1, m2, mnpp.Item1, mnpp.Item2, pmatch, comps);
				matchcount = pmatch.Count;
			}
			else if(comps.ExtRefTargetsToMatchFrontier.Count != 0)
			{
				typeofmatch = 1;
				erpp = comps.ExtRefTargetsToMatchFrontier.First.Value;
				comps.ExtRefTargetsToMatchFrontier.RemoveFirst();
				targetaddr = m1.m_externalrefs[erpp.Item1][erpp.Item2];
				FindMatchesForExternalRefTarget(m1, m2, erpp.Item1, erpp.Item2, extpmatch, comps);
				matchcount = extpmatch.Count;
			}
			else
			{
				typeofmatch = 2;
				evspp = comps.StackTargetMatchFrontier.First.Value;
				comps.StackTargetMatchFrontier.RemoveFirst();
				targetaddr = evspp.Item2.TrgtAddress;
				FindMatchesForStackLocation(m1, m2, evspp.Item1, evspp.Item2, pmatch, comps);
				matchcount = pmatch.Count;
			}

			Tuple<ALocation, ATrgtEnum> mnpp_m2 = null;
			Tuple<AExternalRef, int> erpp_m2 = null;
			Tuple<int, ATrgtEnum> evspp_m2 = null;

			for(int i = 0; i < matchcount; ++i)
			{
				//add edge + node mapping to comps info then rec call
				int nodeidinm2;

				if(typeofmatch == 0)
				{
					nodeidinm2 = pmatch[i].TrgtAddress;
					ALocation nn2 = m2.ResolveRawAddress(comps.AddressMap[mnpp.Item1.Address]);
					mnpp_m2 = new Tuple<ALocation, ATrgtEnum>(nn2, pmatch[i]);
					comps.LocationTargetMatchDoneInM2.Add(mnpp_m2);
				}
				else if(typeofmatch == 1)
				{
					nodeidinm2 = m2.m_externalrefs[erpp.Item1][extpmatch[i]];
					erpp_m2 = new Tuple<AExternalRef, int>(erpp.Item1, extpmatch[i]);
					comps.ExtRefTargetMatchDoneInM2.Add(erpp_m2);
				}
				else
				{
					nodeidinm2 = pmatch[i].TrgtAddress;
					evspp_m2 = new Tuple<int, ATrgtEnum>(evspp.Item1, pmatch[i]);
					comps.StackTargetMatchDoneInM2.Add(evspp_m2);
				}

				bool endNodeAlreadyMapped = comps.AddressMap.ContainsKey(targetaddr);
				int origSize = comps.LocationTargetMatchFrontier.Count;
				if(!endNodeAlreadyMapped)
				{
					//add the node to the map and add all the out edges to the frontier
					//note we add them at the tail and may need to pop them if the match we chose doesn't work
					Contract.Assert(m1.ResolveRawAddress(targetaddr).LocationType == m2.ResolveRawAddress(nodeidinm2).LocationType);
					
					comps.AddressMap.Add(targetaddr, nodeidinm2);
					ALocation enn = m1.ResolveRawAddress(targetaddr);

					IEnumerator<ATrgtEnum> trgenum = enn.GetTargetEnum();
					while(trgenum.MoveNext())
						comps.LocationTargetMatchFrontier.AddLast(new Tuple<ALocation, ATrgtEnum>(enn, trgenum.Current));
				}

				//if sucess, good succed and exit
				bool success = GraphCompareDoIt(m1, m2, comps);
				if(success)
					return success;

				//otherwise unwind matching and onto next
				if(typeofmatch == 0)
					comps.LocationTargetMatchDoneInM2.Remove(mnpp_m2);
				else if(typeofmatch == 1)
					comps.ExtRefTargetMatchDoneInM2.Remove(erpp_m2);
				else
					comps.StackTargetMatchDoneInM2.Remove(evspp_m2);

				comps.ExternalRefMap.Clear();

				if(!endNodeAlreadyMapped)
				{
					comps.AddressMap.Remove(targetaddr);

					//we follow strict fucking stack protocol, don't break it
					int toPopCount = comps.LocationTargetMatchFrontier.Count - origSize;
					for(int pci = 0; pci < toPopCount; ++pci)
						comps.LocationTargetMatchFrontier.RemoveLast();
				}
			}

			//no match found, damit, ok backtrack
			if(typeofmatch == 0)
				comps.LocationTargetMatchFrontier.AddFirst(mnpp);
			else if(typeofmatch == 1)
				comps.ExtRefTargetsToMatchFrontier.AddFirst(erpp);
			else
				comps.StackTargetMatchFrontier.AddFirst(evspp);

			return false;
		}

		/// <summary>
		/// Once we have processed the entire graph at call entry, see if we also have a mapping that is consistent with the external refs, and build the mapping.
		/// </summary>
		private static bool GraphCompareExtRefCallEntry(AProgramMemory m1, AProgramMemory m2, AMemCompareStruct comps)
		{
			Contract.Requires(comps.CompareStyle == AMemCompareStruct.CompareTag.CallEntry);
			Contract.Requires(comps.ExternalRefMap.Count == 0);

			HashSet<AExternalRef> mappedinm2 = new HashSet<AExternalRef>();

			foreach(KeyValuePair<AExternalRef, int[]> m1erp in m1.m_externalrefs)
			{
				Contract.Assert(m1erp.Value.Length == 1);
				int ttl1 = comps.AddressMap[m1erp.Value[0]];

				AExternalRef mapto = null;
				foreach(KeyValuePair<AExternalRef, int[]> m2erp in m2.m_externalrefs)
				{
					if(mappedinm2.Contains(m2erp.Key))
						continue;

					Contract.Assert(m2erp.Value.Length == 1);
					int ttl2 = m2erp.Value[0];
					if((ttl1 == ttl2) & (m1erp.Key.StaticRef == m2erp.Key.StaticRef))
					{
						mapto = m2erp.Key;
						break;
					}
				}

				if(mapto == null)
					return false;
				else
				{
					comps.ExternalRefMap.Add(m1erp.Key, mapto);
					mappedinm2.Add(mapto);
				}
			}

			return true;
		}

		/// <summary>
		/// Initialize all the pending info in <c>comps</c> by loading in all the intial root equalities. 
		/// Return false if an incompatibility is found, true otherwise.
		/// </summary>
		private static bool LoadRootsToPending(AProgramMemory m1, AProgramMemory m2, AMemCompareStruct comps, bool localsonly)
		{
			Contract.Requires(m1 != null && (!m1.IsInfeasable));
			Contract.Requires(m2 != null && (!m2.IsInfeasable));
			Contract.Requires((comps != null) & (comps.AddressMap.Count == 0)); //everything should be 0 but I am too lazy to write all of it out

			Contract.Assert(m1.m_nametonodemap.Count == m2.m_nametonodemap.Count);
			foreach(IRRootIdentifier rr in m1.m_nametonodemap.Keys)
			{
				Contract.Assert(m2.m_nametonodemap.ContainsKey(rr));
				Contract.Assert((!comps.AddressMap.ContainsKey(m1.m_nametonodemap[rr])) || comps.AddressMap[m1.m_nametonodemap[rr]] == m2.m_nametonodemap[rr]);

				if(!comps.AddressMap.ContainsKey(m1.m_nametonodemap[rr]))
				{
					comps.AddressMap.Add(m1.m_nametonodemap[rr], m2.m_nametonodemap[rr]);
					ALocation tl1 = m1.ResolveRawAddress(m1.m_nametonodemap[rr]);
					ALocation tl2 = m2.ResolveRawAddress(m2.m_nametonodemap[rr]);
					Contract.Assert(tl1.LocationType == tl2.LocationType);

					bool locsmatch = ALocation.EqualALocation(tl1, tl2, comps.CompareStyle == AMemCompareStruct.CompareTag.CallEntry, comps.CompareStyle == AMemCompareStruct.CompareTag.CallExit);
					if(!locsmatch)
						return false;

					IEnumerator<ATrgtEnum> trgtenum = tl1.GetTargetEnum();
					while(trgtenum.MoveNext())
						comps.LocationTargetMatchFrontier.AddFirst(new Tuple<ALocation, ATrgtEnum>(tl1, trgtenum.Current));
				}
			}

			if(!localsonly)
			{
				Contract.Assert(m1.m_externalrefs.Count == m2.m_externalrefs.Count);
				foreach(AExternalRef extr in m1.m_externalrefs.Keys)
				{
					Contract.Assert(m2.m_externalrefs.ContainsKey(extr));

					int[] m1l = m1.m_externalrefs[extr];
					int[] m2l = m2.m_externalrefs[extr];
					if(m1l.Length != m2l.Length)
						return false;

					for(int i = 0; i < m1l.Length; ++i)
						comps.ExtRefTargetsToMatchFrontier.AddFirst(new Tuple<AExternalRef, int>(extr, i));
				}

				Contract.Assert(m1.m_evalstack.Count == m2.m_evalstack.Count);
				for(int i = 0; i < m1.m_evalstack.Count; ++i)
				{
					bool evalsequal = m1.m_evalstack[i].EqualEvalStackEntry(m2.m_evalstack[i]);
					if(!evalsequal)
						return false;

					IEnumerator<ATrgtEnum> trgtenum = m1.m_evalstack[i].GetATrgtEnumerator();
					while(trgtenum.MoveNext())
						comps.StackTargetMatchFrontier.AddFirst(new Tuple<int, ATrgtEnum>(i, trgtenum.Current));
				}
			}

			return true;
		}

		/// <summary>
		/// Return true if these graphs can be related based on node/edge counts
		/// </summary>
		[Pure]
		private static bool CheckNodeEdgeAndFixedNameCountOk(AProgramMemory m1, AProgramMemory m2)
		{
			Contract.Requires(m1 != null && (!m1.IsInfeasable));
			Contract.Requires(m2 != null && (!m2.IsInfeasable));

			Contract.Assert(m1.m_evalstack.Count == m2.m_evalstack.Count);
			for(int i = 0; i < m1.m_evalstack.Count; ++i)
			{
				Contract.Assert(m1.m_evalstack[i].SLocType == m2.m_evalstack[i].SLocType);
				if(m1.m_evalstack[i].SLocType is IRPrimitiveType)
					continue;

				if(m1.m_evalstack[i].TotalTargetCount() != m2.m_evalstack[i].TotalTargetCount())
					return false;
			}

			Contract.Assert(m1.m_nametonodemap.Count == m2.m_nametonodemap.Count);
			foreach(IRRootIdentifier nkv in m1.m_nametonodemap.Keys)
			{
				ALocation tl1 = m1.ResolveRawAddress(m1.m_nametonodemap[nkv]);
				ALocation tl2 = m2.ResolveRawAddress(m2.m_nametonodemap[nkv]);

				Contract.Assert(tl1.LocationType == tl2.LocationType);

				if(tl1.TotalTargetCount() != tl2.TotalTargetCount())
					return false;
			}

			if(m1.m_memory.Count != m2.m_memory.Count)
				return false;

			int ncount = m1.m_memory.Count;
			int ec1 = 0; //number of MEdges in m1
			int ec2 = 0; //number of MEdges in m2
			for(int i = 0; i < ncount; ++i)
			{
				ec1 += m1.m_memory[i].TotalTargetCount();
				ec2 += m2.m_memory[i].TotalTargetCount();
			}

			return ec1 == ec2;
		}

		/// <summary>
		/// Use this method to compare 2 graphs for equality at call entry. If there is a match put the computed mapping from m1 to m2 into the two maps.
		/// </summary>
		[Pure]
		internal static bool EquivOnCallEntry(AProgramMemory m1, AProgramMemory m2, CallStateSubMap csm)
		{
			Contract.Requires(m1 != null && (!m1.IsInfeasable));
			Contract.Requires(m2 != null && (!m2.IsInfeasable));

			if(!AProgramMemory.CheckNodeEdgeAndFixedNameCountOk(m1, m2))
				return false;

			if(m1.m_externalrefs.Count != m2.m_externalrefs.Count)
				return false;

			Dictionary<int, int> m1tom2idmap = new Dictionary<int, int>();
			AMemCompareStruct cmps = new AMemCompareStruct(AMemCompareStruct.CompareTag.CallEntry);

			bool loadok = AProgramMemory.LoadRootsToPending(m1, m2, cmps, true);
			if(!loadok)
				return false;
			else
			{
				bool success = AProgramMemory.GraphCompareDoIt(m1, m2, cmps);

				if(success)
				{
					csm.OutCase = MatchCase.EqualityMatch;

					foreach(KeyValuePair<int, int> idm in cmps.AddressMap)
						m1tom2idmap.Add(idm.Key, idm.Value);
					Dictionary<int, HashSet<int>> identitytagmap = m1.ConvertNodeIDMapIntoIdentityTagMap(m1tom2idmap, m2);

					foreach(KeyValuePair<int, HashSet<int>> idm in identitytagmap)
					{
						csm.ResMap.Add(idm.Key, new HashSet<int>());
						csm.ResMap[idm.Key].UnionWith(idm.Value);
					}

					foreach(KeyValuePair<AExternalRef, AExternalRef> erm in cmps.ExternalRefMap)
					{
						csm.ExtRefMap.Add(erm.Key, new HashSet<AExternalRef>());
						csm.ExtRefMap[erm.Key].Add(erm.Value);
					}
				}

				return success;
			}
		}

		/// <summary>
		/// Use this method to compare 2 graphs for strict equality on method exit if we know that the previous exit state 
		/// and this exit state have the same set of identity tags and external ref names.
		/// </summary>
		[Pure]
		internal static bool EquivOnExit(AProgramMemory m1, AProgramMemory m2, Dictionary<int, int> opaddressmap)
		{
			Contract.Requires(m1 != null);
			Contract.Requires(m2 != null);

			if(m1.IsInfeasable & m2.IsInfeasable)
				return true;
			else if(m1.IsInfeasable != m2.IsInfeasable)
				return false;
			else
			{
				if(!AProgramMemory.CheckNodeEdgeAndFixedNameCountOk(m1, m2))
					return false;

				if(m1.m_externalrefs.Count != m2.m_externalrefs.Count)
					return false;

				AMemCompareStruct cmps = new AMemCompareStruct(AMemCompareStruct.CompareTag.CallExit);
				bool loadok = AProgramMemory.LoadRootsToPending(m1, m2, cmps, false);
				if(!loadok)
					return false;
				else
				{
					bool success = AProgramMemory.GraphCompareDoIt(m1, m2, cmps);

					if(success && opaddressmap != null)
					{
						foreach(KeyValuePair<int, int> nidmap in cmps.AddressMap)
							opaddressmap.Add(nidmap.Key, nidmap.Value);
					}

					return success;
				}
			}
		}

		/// <summary>
		/// Use this method to compare 2 graphs for strict equality within a method body loop fixpoint.
		/// </summary>
		[Pure]
		internal static bool EquivOnLoopFix(AProgramMemory m1, AProgramMemory m2)
		{
			Contract.Requires(m1 != null);
			Contract.Requires(m2 != null);

			if(m1.IsInfeasable & m2.IsInfeasable)
				return true;
			else if(m1.IsInfeasable != m2.IsInfeasable)
				return false;
			else
			{
				if(!AProgramMemory.CheckNodeEdgeAndFixedNameCountOk(m1, m2))
					return false;

				AMemCompareStruct cmps = new AMemCompareStruct(AMemCompareStruct.CompareTag.LoopFix);
				bool loadok = AProgramMemory.LoadRootsToPending(m1, m2, cmps, false);
				if(!loadok)
					return false;
				else
				{
					bool success = AProgramMemory.GraphCompareDoIt(m1, m2, cmps);
					return success;
				}
			}
		}

		/// <summary>
		/// Fill in the call state map (going from this -> other) and check if this subsumes other or not.
		/// Set all the values in csm as needed.
		/// </summary>
		internal void BuildCallStateMapForSubsume_OptionalCheckSubsume(AProgramMemory other, AMemEqPartition eqp, CallStateSubMap csm, bool dosubsumecheck)
		{
			List<ALocation> tmergefromthis = new List<ALocation>();
			List<ALocation> tmergefromother = new List<ALocation>();
			Dictionary<ALocation, List<ALocation>> thistoothernodemap = new Dictionary<ALocation, List<ALocation>>();
			//first build the mapping from nodes in this to nodes in other, while we are doing this see if we can build an
			//isomorphism between this and the partition.
			bool isofound = true;
			foreach(AMemPartEqClass eqc in eqp.PartIDToEqClassMap.Values)
			{
				for(int i = 0; i < eqc.PartitionTypes.Count; ++i)
				{
					tmergefromthis.Clear();
					tmergefromother.Clear();
					AProgramMemory.ExtractNodesFromPartitionBasedOnSource(eqc, eqc.PartitionTypes[i], this, tmergefromthis, other, tmergefromother);

					foreach(ALocation nn in tmergefromthis)
						thistoothernodemap.Add(nn, new List<ALocation>(tmergefromother));

					if(tmergefromthis.Count != 1)
						isofound = false;
				}
			}

			//now compute the identity map
			foreach(KeyValuePair<ALocation, List<ALocation>> nkvp in thistoothernodemap)
			{
				HashSet<int> idrmp = new HashSet<int>();
				for(int i = 0; i < nkvp.Value.Count; ++i)
					idrmp.UnionWith(nkvp.Value[i].IdentityTags);

				for(int j = 0; j < nkvp.Key.IdentityTags.Length; ++j)
				{
					int idt = nkvp.Key.IdentityTags[j];
					if(!csm.ResMap.ContainsKey(idt))
						csm.ResMap.Add(idt, new HashSet<int>());
					csm.ResMap[idt].UnionWith(idrmp);
				}
			}

			//build a map from nodes in other to the external refs that refer to them
			Dictionary<ALocation, List<AExternalRef>> extrmap = new Dictionary<ALocation, List<AExternalRef>>();
			foreach(KeyValuePair<AExternalRef, int[]> ekvp in other.m_externalrefs)
			{
				for(int i = 0; i < ekvp.Value.Length; ++i)
				{
					ALocation nn = other.m_memory[ekvp.Value[i]];
					if(!extrmap.ContainsKey(nn))
						extrmap.Add(nn, new List<AExternalRef>());
					extrmap[nn].Add(ekvp.Key);
				}
			}

			//next the external ref map
			foreach(KeyValuePair<AExternalRef, int[]> ekvp in this.m_externalrefs)
			{
				csm.ExtRefMap.Add(ekvp.Key, new HashSet<AExternalRef>());

				for(int i = 0; i < ekvp.Value.Length; ++i)
				{
					ALocation thisnn = this.m_memory[ekvp.Value[i]];
					foreach(ALocation othernn in thistoothernodemap[thisnn])
					{
						if(extrmap.ContainsKey(othernn))
							csm.ExtRefMap[ekvp.Key].UnionWith(extrmap[othernn]);
					}
				}
			}

			if(!dosubsumecheck)
				csm.OutCase = MatchCase.SubsumeMatch;
			else
			{
				//finally if we have an isomorphism then remap this, merge it with other and compare the result with this
				//this gives us the subsume thing which we use to set the flag in <c>csm</c>;
				bool equalonentry = false;
				if(isofound)
				{
					AProgramMemory prename = this.CopyMemoryState();
					prename.MapIntoResForFinalResult(csm);
					prename.CleanInfeasibleNodes();
					prename.NormalizeAtRecursiveCallEntry();

					AProgramMemory jpm = AProgramMemory.PMemoryMergeCallsEntry(prename, other);
					CallStateSubMap equivcsm = new CallStateSubMap();
					equalonentry = AProgramMemory.EquivOnCallEntry(jpm, prename, equivcsm); //not this because we could remove nodes in cleaninfeasible
				}

				if(equalonentry)
					csm.OutCase = MatchCase.SubsumeMatch;
				else
					csm.OutCase = MatchCase.SubsumeAlter;
			}
		}
	}

	/// <summary>
	/// Defines a class to handle the generalizede comparision of two graphs. 
	/// </summary>
	internal sealed class AMemCompareStruct
	{
		internal enum CompareTag
		{
			CallEntry,
			CallExit,
			LoopFix
		}

		/// <summary>
		/// The map of Address to Address that defines the isomorphism we are building.
		/// </summary>
		internal readonly Dictionary<int, int> AddressMap;

		/// <summary>
		/// The map of ext refs to ext refs that defines the isomorphism we are building (only at call entry).
		/// </summary>
		internal readonly Dictionary<AExternalRef, AExternalRef> ExternalRefMap;

		/// <summary>
		/// The currently pending Location/trgt offsets that need to be matched.
		/// </summary>
		internal readonly LinkedList<Tuple<ALocation, ATrgtEnum>> LocationTargetMatchFrontier;

		/// <summary>
		/// The currently pending stackpos/trgt offsets that need to be matched from stack locations.
		/// </summary>
		internal readonly LinkedList<Tuple<int, ATrgtEnum>> StackTargetMatchFrontier;

		/// <summary>
		/// The currently pending external reference targets that need to matched.
		/// </summary>
		internal readonly LinkedList<Tuple<AExternalRef, int>> ExtRefTargetsToMatchFrontier;

		/// <summary>
		/// The Location/target offsets that have been be matched in <c>m2</c>.
		/// </summary>
		internal readonly HashSet<Tuple<ALocation, ATrgtEnum>> LocationTargetMatchDoneInM2;

		/// <summary>
		/// The stackpos/target offsets that have been matched in <c>m2</c>.
		/// </summary>
		internal readonly HashSet<Tuple<int, ATrgtEnum>> StackTargetMatchDoneInM2;

		/// <summary>
		/// Theexternal reference targets that have been matched in <c>m2</c>.
		/// </summary>
		internal readonly HashSet<Tuple<AExternalRef, int>> ExtRefTargetMatchDoneInM2;

		/// <summary>
		/// Select the type of match we want to do.
		/// </summary>
		internal readonly CompareTag CompareStyle;

		internal AMemCompareStruct(CompareTag cstyle)
		{
			this.AddressMap = new Dictionary<int, int>();
			this.ExternalRefMap = new Dictionary<AExternalRef, AExternalRef>();

			this.LocationTargetMatchFrontier = new LinkedList<Tuple<ALocation, ATrgtEnum>>();
			this.StackTargetMatchFrontier = new LinkedList<Tuple<int, ATrgtEnum>>();
			this.ExtRefTargetsToMatchFrontier = new LinkedList<Tuple<AExternalRef, int>>();

			this.LocationTargetMatchDoneInM2 = new HashSet<Tuple<ALocation, ATrgtEnum>>();
			this.StackTargetMatchDoneInM2 = new HashSet<Tuple<int, ATrgtEnum>>();
			this.ExtRefTargetMatchDoneInM2 = new HashSet<Tuple<AExternalRef, int>>();

			this.CompareStyle = cstyle;
		}
	}
}
